Inference at * 1 
Iof proof for Lemma not assert elim:



1. b : 
2. (b)
  b = ff 

latex

 by BoolInd 1 

latex

 1: 

 1: 1. (tt)
 1:   tt = ff
 2: 

 2: 1. (ff)
 2:   ff = ff
 .

Definitions

t  T, Unit, , tt, , ff